All four people start out on the southern side of the bridge, namely the King, Queen, a young Lady and a Knight. The goal is for everyone to arrive at the castle- the north of the bridge, before the time runs out. The bridge can hold at most two people at a time and they must be carrying the torch when crossing the bridge. The King needs 5 minutes to cross, the Queen 10 minutes, the Lady 2 minutes and the Knight 1 minute. The question is given a specific amount of time, whether all people can cross the bridge in time.

The following statement models the system.

• #define Max 17;
• #define KNIGHT 1;
• #define LADY 2;
• #define KING 5;
• #define QUEEN 10;

The above defines the constants in this model, where #define  is a reserved keyword for defining a synonymy for a (integer or Boolean) constant or a proposition.  Max represents the maximum number of time units. KNIGHT stands for the number of time units the knight needs. Similarly, we define the rest ones.  We remark the users shall use constants (instead of variables) whenever possible. Because constants never change, during verification they are not excluded from the system state information, and hence, using constants instead of variables save memory and maybe time also.

• var Knight = 0;
• var Lady = 0;
• var King = 0;
• var Queen = 0;
• var time;

The above defines the variables in the system, where var is reserved keyword for introducing variables or arrays. Notice that PAT has a weak type system. Variable Knight is used to model whether the knight is at the southern side of the bridge or the northern side. It is of value 0 if the knight hasn't crossed the bridge, otherwise 1. Similarly, we define the rest. Variable time records the number of time units spent by far. The default value is 0.  

South() = [time <= Max && Knight == 0 && Lady == 0]go_knight_lady{Knight = 1; Lady= 1; time = time+LADY;} -> North()
                 [] [time <= Max && Knight == 0 && King == 0]go_knight_king{Knight = 1; King= 1; time = time+KING;} -> North()       
                 [] [time <= Max && Knight == 0 && Queen == 0]go_knight_queen{Knight = 1; Queen= 1; time = time+QUEEN;} -> North()
                 [] [time <= Max && Lady == 0 && King == 0]go_lady_king{Lady = 1; King= 1; time = time+KING;} -> North()
                 [] [time <= Max && Lady == 0 && Queen == 0]go_lady_queen{Lady = 1; Queen= 1; time = time+QUEEN;} -> North()
                 [] [time <= Max && King == 0 && Queen == 0]go_king_queen{King = 1; Queen= 1; time = time+QUEEN;} -> North()
                 [] [time <= Max && Knight == 0]go_knight{Knight = 1; time = time+KNIGHT;} -> North()
                 [] [time <= Max && Lady == 0]go_lady{Lady = 1; time = time+LADY;} -> North()
                 [] [time <= Max && King == 0]go_king{King = 1; time = time+KING;} -> North()
                 [] [time <= Max && Queen == 0]go_queen{Queen = 1; time = time+QUEEN;} -> North();

The above defines a process named South(), which models the system behaviors when the torch is at the southern side  of the bridge. Naturally, there are multiple ways the people can cross the bridge. Each way is modeled as one line in the following form,

[condition]event{code} -> North()  

Informally, it means that if the condition is true, then the event can occur, i.e., the code attached with the event can be executed. Notice that code here could contain while-loops, if-then-else, etc. For instance, at the first line, the condition states that the time is not be used up yet, the Knight and the Lady  are both at the southern side of the bridge. If this is true, then the event go_knight_lady can occur, which in terms means that the variable Knight and Lady are set to be 1 (meaning they have crossed the bridge) and time is incremented by the number of time units needed by the lady. After that, the system behaves as process North, which will be defined later. Similarly, we can enumerate all possible ways of crossing the bridge, e.g., the knight goes together with the king or queen, the king goes with the lady or queen, and the queen goes with the lady. Notice that the operator '[] ' denotes choice. That is, either one of the ways may occur. Choice is one of many useful compositional operators offered in PAT. 

North() = [time <= Max && Knight == 1 && Lady == 1]back_knight_lady{Knight = 0; Lady = 0; time = time+LADY;} -> South()
                [] [time <= Max && Knight == 1 && King == 1]back_knight_king{Knight = 0; King = 0; time = time+KING;} -> South()
                [] [time <= Max && Knight == 1 && Queen == 1]back_knight_queen{Knight = 0; Queen = 0; time = time+QUEEN;} -> South()
                [] [time <= Max && Lady == 1 && King == 1]back_lady_king{Lady = 0; King = 0; time = time+KING;} -> South()
                [] [time <= Max && Lady == 1 && Queen == 1]back_lady_queen{Lady = 0; Queen = 0; time = time+QUEEN;} -> South()
                [] [time <= Max && King == 1 && Queen == 1]back_king_queen{King = 0; Queen = 0; time = time+QUEEN;} -> South()
                [] [time <= Max && Knight == 1]back_knight{Knight = 0; time = time+KNIGHT;} -> South()
                [] [time <= Max && Lady == 1]back_lady{Lady = 0; time = time+LADY;} -> South()
                [] [time <= Max && King == 1]back_king{King = 0; time = time+KING;} -> South()
                [] [time <= Max && Queen == 1]back_queen{Queen = 0; time = time+QUEEN;} -> South();

In a very similar and simple way, the above defines process North, in terms of what are the possible ways of crossing the bridge when the torch is at the northern side of the bridge. Notice that in process North(), process South() is invoked. This forms a mutual recursion, which is perfectly normal and safe in PAT. Having modeled all possible behaviors of the systems as the above processes, we are now ready to reason about the system. 

• #define goal (time<=Max && Knight==1 && Lady==1 && King==1 && Queen==1);
• #assert South() reaches goal;

The question we are interested is whether it is feasible to cross the bridge within Max number of time unit. The above shows one of the questions. The first line defines a proposition named goal, which states that the time taken should be not greater than Max and all people should be on the northern side of the bridge. The second line is the assertion, where #assert is a reserved keyword.  'reaches' is also a keyword. Informally, the assertion says that  starting from process South(), we will reach a state at which the proposition goal is true. Notice that this is a reachability analysis task. Alternatively, we could define an LTL assertion as follows,  

#assert South() |= [] !goal;

where '[] ' is the temporal operator, which reads as "always" and '! ' is the negation operator. Notice that '[] ' in process definition has a different meaning with assertions. Informally speaking, this assertion says that starting from process South(), every system state reached satisfies the proposition "!goal". A counterexample to this assertion would be a trace which leads to a state where "goal" is satisfied.                

After modeling, you may either simulate the model by pressing F6 or click the Simulation button, or verify it by pressing F7 or click the Verification button. Once you click the Simulation button, a window will be prompt. You can choose process from a drop-list at the left top corner. Notice that only processes without parameters are available for selection. After click the Verification button, a verification window will be prompt. All assertions are listed. Double-click one of them or click the Verify button will trigger the model checker to perform the task. There are a number options to choose from. For now, we will simply use the default setting. In the example, you can select the first assertion, and click Verify, a trace which leads to a state where "goal" is true is printed.  If you click the "Simulate Counter Example" button, the simulator is prompt with the trace visualized.